(set-logic QF_BV)
;(set-option :model_validate true)
(set-option :model true)
(set-option :sat.threads 3)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const bv_7-0 (_ BitVec 7))
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(assert (or v8 v1 v16 v1 v1 v7 v9 v8))
(assert-soft (or v7 v16 v9))
(assert (or v16 v9 v16 v1))
(assert-soft (or v9))
(assert-soft (or v9 v8 v1 v8 v8))
(assert (or v16))
(assert-soft (or v8 v8))
(assert (or v1 v7))
(assert (or v16 v8))
(assert (or v16 v9 v8 v16))
(assert (or v7))
(assert-soft (or v16))
(assert (or v16 v8 v7 v8 v9 v16))
(check-sat)
(exit)
